K Framework - Installation and Basic Usage for Smart Contract Formal Verification

---

Slide 1: What is K Framework?

• Definition: The K Framework is a platform for defining programming languages, formalizing semantics, and verifying properties of programs.
• Key Features:
  • Formal specification of programming languages.
  • Automatically generates execution engines and verification tools.
  • Ideal for verifying smart contracts due to its precision in handling formal semantics.

---

Slide 2: Why Use K Framework for Smart Contracts?

• Why Formal Verification Matters:

  • Smart contracts handle significant amounts of funds and sensitive data.
  • Bugs or vulnerabilities can lead to serious losses.
  • Formal verification ensures correctness by mathematically proving contract behavior under all possible conditions.

• Benefits of K Framework:

  • Provides a rigorous approach to ensuring smart contracts function as expected.
  • Enables formalization of the contract’s logic in an executable specification.
  • Allows for automated testing and verification.

---

Slide 3: Installing K Framework

1. Pre-requisites:

   • Ubuntu (or any Linux distro)
   • Java 8 or later
   • Haskell
   • Z3 Theorem Prover (optional but recommended for formal verification)

2. Installation Steps:

   1. Install Binaries from:
      https://github.com/runtimeverification/k/releases/tag/v7.1.155

   2. Verify Installation:

      • Check by running the command:

        kompile --version
        

---

Slide 4: K Framework Basics

• K Definition Structure:

  • Modules: Contain the syntax and rules that define a language.
  • Syntax: Defines the grammar of the smart contract language.
  • Rules: Specify the operational semantics (how the contract behaves).

• Smart Contract Representation:

  • A smart contract is modeled in K using its language constructs.
  • K captures the state of a contract and the logic governing state transitions.

---

Slide 5: Formal Verification Using K

• Goal: Prove that a smart contract meets its specification without error.

• Steps to Formal Verification:

  1. Define the contract’s behavior using K syntax and rules.
  2. Model the state and transitions of the contract.
  3. Specify properties and invariants that the contract must satisfy (e.g., no funds can be lost, only specific users can withdraw, etc.).
  4. Use the K prover to verify the contract against the defined properties.

---

Slide 6: Example Smart Contract: Token Transfer

• Problem Statement:

  • A simple token contract that allows users to transfer tokens from one account to another.

• Basic Contract Logic:

  function transfer(address sender, address receiver, uint amount) public {
      require(balance[sender] >= amount, "Insufficient funds");
      balance[sender] -= amount;
      balance[receiver] += amount;
  }
  

• Key Properties to Verify:

  1. Balance Preservation: Total supply of tokens is unchanged after transfer.
  2. Sender Has Enough Balance: The sender can’t send more tokens than they own.

---

Slide 7: Formalizing the Token Contract in K

• Define Syntax:

  syntax Contract ::= "transfer" "(" Address "," Address "," Int ")" 
  syntax Int ::= balance(Address)
  

• Define Rules:

  rule <k> transfer(S, R, A) => . ... </k>
       <balance> (S |-> BS => BS - A)
                 (R |-> BR => BR + A)
                 ...
       requires BS >= A
  

• Property to Verify (Balance Preservation):

  claim <k> transfer(S, R, A) => . ... </k>
        <balance> (S |-> BS) (R |-> BR) => <balance> (S |-> BS - A) (R |-> BR + A)
        ensures BS + BR == BS' + BR'
  

---

Slide 8: Running Formal Verification

1. Compile the Contract:

   kompile contract.k
   

2. Prove Properties:

   krun --prove contract-verification-spec.k
   

3. Output:

   • If the proof is successful, K Framework confirms that the smart contract satisfies all the specified properties.

---